$\forall$$a$:Id, $T$:Top, ${\it ds}$:$x$:Id fp$\rightarrow$ Top, $P$:Top, ${\it init}$:$x$:Id fp$\rightarrow$ Top, $l$:IdLnk, ${\it tg}$:Id, $L$:Knd List.
\\[0ex]with ds: ${\it ds}$ init: ${\it init}$action $a$:$T$ precondition $a$(v) is $P$ $\Vert\!+$ only $L$ sends on ($l$ with ${\it tg}$)